LeanMachineLearning exposition

Bandits.«term𝓛[_|_←_;_]»🔗

Minimal Lean file

term𝓛[_|_←_;_]🔗

DefinitionBandits.«term𝓛[_|_←_;_]»
Details

Law of Y conditioned on the event that X equals x.

🔗def
Bandits.«term𝓛[_|_←_;_]» : Lean.ParserDescr
Bandits.«term𝓛[_|_←_;_]» :
  Lean.ParserDescr

Code

notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}])

Actions: Source · Open Issue